(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i12 Int)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const i16 Int)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const i17 Int)
(declare-const v9 Bool)
(declare-const i18 Int)
(assert (or v9 (= 48 i1) (distinct i5 i2)))
(assert-soft (or v9 v1 (and (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v3 v4 v5 (>= i1 87) (=> (< 93 646) v6) v5 (=> (< 93 646) v6) (distinct i5 i2))))
(assert (or (distinct i5 i2) (distinct i5 i2) v9))
(assert (or (= 48 i1) (>= i1 87) (distinct i5 i2)))
(assert-soft (or (distinct i5 i2) v9 (>= i1 87)))
(assert (or v6 (distinct i5 i2) (distinct i5 i2)))
(assert (or (distinct i5 i2) v5 (distinct i5 i2)))
(assert (or (>= i1 87) v5 v5))
(assert (or (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) (= 48 i1) (and (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v3 v4 v5 (>= i1 87) (=> (< 93 646) v6) v5 (=> (< 93 646) v6) (distinct i5 i2))))
(assert-soft (or v6 (distinct i5 i2) (= 48 i1)))
(assert (or v1 v9 (distinct i5 i2)))
(assert-soft (or v1 v5 v9))
(assert (or (distinct i5 i2) (distinct i5 i2) (= 48 i1)))
(assert-soft (or (>= i1 87) (>= i1 87) v1))
(assert (or v9 (and (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v3 v4 v5 (>= i1 87) (=> (< 93 646) v6) v5 (=> (< 93 646) v6) (distinct i5 i2)) (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646))))
(assert (or (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) (distinct i5 i2) (distinct i5 i2)))
(assert-soft (or v1 v9 v9))
(assert (or (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) (= 48 i1) v1))
(assert (or (>= i1 87) (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v9))
(assert (or (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v5 (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646))))
(assert (or (>= i1 87) (>= i1 87) (>= i1 87)))
(assert (or (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) (= 48 i1) (and (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v3 v4 v5 (>= i1 87) (=> (< 93 646) v6) v5 (=> (< 93 646) v6) (distinct i5 i2))))
(assert (or (distinct i5 i2) v1 v9))
(assert (or v1 v9 v1))
(assert (or v5 (distinct i5 i2) v6))
(assert-soft (or v5 v6 v1))
(assert-soft (or v5 (and (= (>= i1 87) v0 v6 v5 (= 48 i1) v5 v1 (>= i1 87) (< 93 646)) v3 v4 v5 (>= i1 87) (=> (< 93 646) v6) v5 (=> (< 93 646) v6) (distinct i5 i2)) v9))
(check-sat)
(exit)

;(set-option :smt.threads 2)
(assert (forall ((a Int) (b Int)) 
(exists ((x Int)) (and (< a (* 20 x)) (< (* 20 x) b))))) 
(apply qe)